The complexity and the significant of software have dramatically increased during the last decades. Some software verification techniques are being developed in order to test programs while other model checking techniques verify that the program operates according to expectations.
There are various types of software verification tools. A first type of software verification tools, model checkers, such as but not limited to ExpliSAT® of IBM®, deterministically check all possible behaviors of a program. These first type software verification tools maintain a record of paths that were checked in order to prevent double checking of the same path.
A second type of software verification tools, such as but not limited to ConTest® of IBM®, randomly check program paths. It does not track the paths that it already checked and randomly selects (at non-deterministic selection points) a successor state (or path) from a uniform distribution over all successors. Accordingly, the chances of checking paths that include many non-deterministic branching points are lower than the chances of checking paths that include fewer non-deterministic branching points.
Due to the random nature of the second type of software model checking tools it is impossible to define a required testing period that will guarantee that all the paths of a program were checked.
The following articles, U.S. patents and patent applications, all being incorporated herein by reference, illustrate various software testing systems and devices that use random schedulers for testing software: U.S. patent application publication serial number 2005/0166202 of Gerell et al., U.S. patent application publication serial number 2004/0210900 of Jones et al., U.S. Pat. No. 6,557,120 of Nicholson et al., “Random Testing of Interrupt-Driven Software”, John Regher, EMSOFT'02, September 2005, pages 19-22, Jersey City, N.J. U.S.A.
There is a need to provide efficient devices, methods and computer program products for checking software entities.